0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 111 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 MRRProof (⇔, 147 ms)
↳34 QDP
↳35 DependencyGraphProof (⇔, 0 ms)
↳36 TRUE
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U4_GGA(X, Y, Z, even_in_ga(s(X), B))
TIMES_IN_GGA(s(X), Y, Z) → EVEN_IN_GA(s(X), B)
EVEN_IN_GA(s(s(X)), B) → U1_GA(X, B, even_in_ga(X, B))
EVEN_IN_GA(s(s(X)), B) → EVEN_IN_GA(X, B)
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → U5_GGA(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → IF_IN_GGGA(B, s(X), Y, Z)
IF_IN_GGGA(true, s(X), Y, Z) → U6_GGGA(X, Y, Z, half_in_ga(s(X), X1))
IF_IN_GGGA(true, s(X), Y, Z) → HALF_IN_GA(s(X), X1)
HALF_IN_GA(s(s(X)), s(Y)) → U2_GA(X, Y, half_in_ga(X, Y))
HALF_IN_GA(s(s(X)), s(Y)) → HALF_IN_GA(X, Y)
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → U7_GGGA(X, Y, Z, times_in_gga(X1, Y, Y1))
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → TIMES_IN_GGA(X1, Y, Y1)
U7_GGGA(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_GGGA(X, Y, Z, plus_in_gga(Y1, Y1, Z))
U7_GGGA(X, Y, Z, times_out_gga(X1, Y, Y1)) → PLUS_IN_GGA(Y1, Y1, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U3_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
IF_IN_GGGA(false, s(X), Y, Z) → U9_GGGA(X, Y, Z, times_in_gga(X, Y, U))
IF_IN_GGGA(false, s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U9_GGGA(X, Y, Z, times_out_gga(X, Y, U)) → U10_GGGA(X, Y, Z, plus_in_gga(Y, U, Z))
U9_GGGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U4_GGA(X, Y, Z, even_in_ga(s(X), B))
TIMES_IN_GGA(s(X), Y, Z) → EVEN_IN_GA(s(X), B)
EVEN_IN_GA(s(s(X)), B) → U1_GA(X, B, even_in_ga(X, B))
EVEN_IN_GA(s(s(X)), B) → EVEN_IN_GA(X, B)
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → U5_GGA(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → IF_IN_GGGA(B, s(X), Y, Z)
IF_IN_GGGA(true, s(X), Y, Z) → U6_GGGA(X, Y, Z, half_in_ga(s(X), X1))
IF_IN_GGGA(true, s(X), Y, Z) → HALF_IN_GA(s(X), X1)
HALF_IN_GA(s(s(X)), s(Y)) → U2_GA(X, Y, half_in_ga(X, Y))
HALF_IN_GA(s(s(X)), s(Y)) → HALF_IN_GA(X, Y)
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → U7_GGGA(X, Y, Z, times_in_gga(X1, Y, Y1))
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → TIMES_IN_GGA(X1, Y, Y1)
U7_GGGA(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_GGGA(X, Y, Z, plus_in_gga(Y1, Y1, Z))
U7_GGGA(X, Y, Z, times_out_gga(X1, Y, Y1)) → PLUS_IN_GGA(Y1, Y1, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U3_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
IF_IN_GGGA(false, s(X), Y, Z) → U9_GGGA(X, Y, Z, times_in_gga(X, Y, U))
IF_IN_GGGA(false, s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U9_GGGA(X, Y, Z, times_out_gga(X, Y, U)) → U10_GGGA(X, Y, Z, plus_in_gga(Y, U, Z))
U9_GGGA(X, Y, Z, times_out_gga(X, Y, U)) → PLUS_IN_GGA(Y, U, Z)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
HALF_IN_GA(s(s(X)), s(Y)) → HALF_IN_GA(X, Y)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
HALF_IN_GA(s(s(X)), s(Y)) → HALF_IN_GA(X, Y)
HALF_IN_GA(s(s(X))) → HALF_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
EVEN_IN_GA(s(s(X)), B) → EVEN_IN_GA(X, B)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
EVEN_IN_GA(s(s(X)), B) → EVEN_IN_GA(X, B)
EVEN_IN_GA(s(s(X))) → EVEN_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → IF_IN_GGGA(B, s(X), Y, Z)
IF_IN_GGGA(true, s(X), Y, Z) → U6_GGGA(X, Y, Z, half_in_ga(s(X), X1))
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → TIMES_IN_GGA(X1, Y, Y1)
TIMES_IN_GGA(s(X), Y, Z) → U4_GGA(X, Y, Z, even_in_ga(s(X), B))
IF_IN_GGGA(false, s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U4_gga(X, Y, Z, even_in_ga(s(X), B))
even_in_ga(0, true) → even_out_ga(0, true)
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
U4_gga(X, Y, Z, even_out_ga(s(X), B)) → U5_gga(X, Y, Z, if_in_ggga(B, s(X), Y, Z))
if_in_ggga(true, s(X), Y, Z) → U6_ggga(X, Y, Z, half_in_ga(s(X), X1))
half_in_ga(0, 0) → half_out_ga(0, 0)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U6_ggga(X, Y, Z, half_out_ga(s(X), X1)) → U7_ggga(X, Y, Z, times_in_gga(X1, Y, Y1))
U7_ggga(X, Y, Z, times_out_gga(X1, Y, Y1)) → U8_ggga(X, Y, Z, plus_in_gga(Y1, Y1, Z))
plus_in_gga(0, Y, Y) → plus_out_gga(0, Y, Y)
plus_in_gga(s(X), Y, s(Z)) → U3_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U3_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U8_ggga(X, Y, Z, plus_out_gga(Y1, Y1, Z)) → if_out_ggga(true, s(X), Y, Z)
if_in_ggga(false, s(X), Y, Z) → U9_ggga(X, Y, Z, times_in_gga(X, Y, U))
U9_ggga(X, Y, Z, times_out_gga(X, Y, U)) → U10_ggga(X, Y, Z, plus_in_gga(Y, U, Z))
U10_ggga(X, Y, Z, plus_out_gga(Y, U, Z)) → if_out_ggga(false, s(X), Y, Z)
U5_gga(X, Y, Z, if_out_ggga(B, s(X), Y, Z)) → times_out_gga(s(X), Y, Z)
U4_GGA(X, Y, Z, even_out_ga(s(X), B)) → IF_IN_GGGA(B, s(X), Y, Z)
IF_IN_GGGA(true, s(X), Y, Z) → U6_GGGA(X, Y, Z, half_in_ga(s(X), X1))
U6_GGGA(X, Y, Z, half_out_ga(s(X), X1)) → TIMES_IN_GGA(X1, Y, Y1)
TIMES_IN_GGA(s(X), Y, Z) → U4_GGA(X, Y, Z, even_in_ga(s(X), B))
IF_IN_GGGA(false, s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
half_in_ga(s(s(X)), s(Y)) → U2_ga(X, Y, half_in_ga(X, Y))
even_in_ga(s(0), false) → even_out_ga(s(0), false)
even_in_ga(s(s(X)), B) → U1_ga(X, B, even_in_ga(X, B))
U2_ga(X, Y, half_out_ga(X, Y)) → half_out_ga(s(s(X)), s(Y))
U1_ga(X, B, even_out_ga(X, B)) → even_out_ga(s(s(X)), B)
half_in_ga(0, 0) → half_out_ga(0, 0)
even_in_ga(0, true) → even_out_ga(0, true)
U4_GGA(X, Y, even_out_ga(B)) → IF_IN_GGGA(B, s(X), Y)
IF_IN_GGGA(true, s(X), Y) → U6_GGGA(Y, half_in_ga(s(X)))
U6_GGGA(Y, half_out_ga(X1)) → TIMES_IN_GGA(X1, Y)
TIMES_IN_GGA(s(X), Y) → U4_GGA(X, Y, even_in_ga(s(X)))
IF_IN_GGGA(false, s(X), Y) → TIMES_IN_GGA(X, Y)
half_in_ga(s(s(X))) → U2_ga(half_in_ga(X))
even_in_ga(s(0)) → even_out_ga(false)
even_in_ga(s(s(X))) → U1_ga(even_in_ga(X))
U2_ga(half_out_ga(Y)) → half_out_ga(s(Y))
U1_ga(even_out_ga(B)) → even_out_ga(B)
half_in_ga(0) → half_out_ga(0)
even_in_ga(0) → even_out_ga(true)
half_in_ga(x0)
even_in_ga(x0)
U2_ga(x0)
U1_ga(x0)
IF_IN_GGGA(false, s(X), Y) → TIMES_IN_GGA(X, Y)
half_in_ga(s(s(X))) → U2_ga(half_in_ga(X))
even_in_ga(s(0)) → even_out_ga(false)
even_in_ga(s(s(X))) → U1_ga(even_in_ga(X))
POL(0) = 0
POL(IF_IN_GGGA(x1, x2, x3)) = x1 + x2 + x3
POL(TIMES_IN_GGA(x1, x2)) = 2·x1 + x2
POL(U1_ga(x1)) = 2·x1
POL(U2_ga(x1)) = 2 + 2·x1
POL(U4_GGA(x1, x2, x3)) = 1 + 2·x1 + x2 + x3
POL(U6_GGGA(x1, x2)) = x1 + x2
POL(even_in_ga(x1)) = x1
POL(even_out_ga(x1)) = x1
POL(false) = 0
POL(half_in_ga(x1)) = x1
POL(half_out_ga(x1)) = 2·x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 0
U4_GGA(X, Y, even_out_ga(B)) → IF_IN_GGGA(B, s(X), Y)
IF_IN_GGGA(true, s(X), Y) → U6_GGGA(Y, half_in_ga(s(X)))
U6_GGGA(Y, half_out_ga(X1)) → TIMES_IN_GGA(X1, Y)
TIMES_IN_GGA(s(X), Y) → U4_GGA(X, Y, even_in_ga(s(X)))
U2_ga(half_out_ga(Y)) → half_out_ga(s(Y))
U1_ga(even_out_ga(B)) → even_out_ga(B)
half_in_ga(0) → half_out_ga(0)
even_in_ga(0) → even_out_ga(true)
half_in_ga(x0)
even_in_ga(x0)
U2_ga(x0)
U1_ga(x0)